docs: clarify X3DH primitive interfaces and passive-secrecy game#3
Conversation
Document current scope (deterministic, no keygen) and what extensions are needed for security proofs (probabilistic encaps, keygen). Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Document current scope (deterministic, no nonce) and what extensions are needed for security proofs (nonce parameter, probabilistic encrypt). Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Document the lowercase/uppercase private/public key convention and replace ASCII SK_B with SKᵦ for consistency with SKₐ. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
- Expand the game description to list the 5 specific private keys (ikₐ, ekₐ, ikᵦ, spkᵦ, opkᵦ) and note that the random key is sampled from SK (the KDF's output space) - Explain why T is embedded at DH3 specifically: it's the only DH value whose computation needs both secret scalars hidden in the DDH challenge (ekₐ, spkᵦ); the other DH values each involve at least one scalar the reduction samples itself Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
ChristianoBraga
left a comment
ChristianoBraga
left a comment
There was a problem hiding this comment.
@jinxinglim could you please answer my comment?
| embeds T as DH3, queries the ROM on the resulting DH tuple to | ||
| get a session key, and passes it directly to the adversary. | ||
|
|
||
| Why DH3? Among the four X3DH DH values, DH3 = ekₐ • SPKᵦ is the |
There was a problem hiding this comment.
Could you revise and elaborate this further?
There was a problem hiding this comment.
Oh. While I was reading through this file, I was wondering why do we embeds T as DH3 and not other DH. So wanted this paragraph to briefly explains why DH3 was chosen to be embedded by T. Perhaps it is not clear in my explanation. The following is an updated version of it:
"""
Why the reduction embeds T as DH3? The DDH challenge fixes two group elements (A, B) whose discrete logs are hidden from the reduction; these are installed as EKₐ and SPKᵦ in the simulated game, while ikₐ, ikᵦ, opkᵦ are sampled by the reduction itself. Of the four DH values, three can then be computed directly from the public keys and the reduction's own scalars: DH1 = ikₐ • SPKᵦ uses ikₐ, and DH2 = ekₐ • IKᵦ, DH4 = ekₐ • OPKᵦ are recovered via DH commutativity as ikᵦ • EKₐ and opkᵦ • EKₐ. DH3 = ekₐ • SPKᵦ is the only one requiring both hidden scalars — exactly the product ab • g that the challenge T encodes. So T is embedded at DH3, and the rest of the tuple is filled in honestly.
"""
WDYT? If you think providing more explanation may be even more confusing, then we can simply remove this newly added paragraph completely.
|
The new paragraph should stay and I like the new prose.
Thank you Jin!
Em dom., 3 de mai. de 2026 às 22:58, Lim Jin Xing ***@***.***>
escreveu:
… ***@***.**** commented on this pull request.
------------------------------
In PQXDHLean/X3DH/X3DHPassiveMessageSecrecy.lean
<#3 (comment)>
:
> @@ -170,6 +173,13 @@ The reduction receives the DDH challenge `(g, EKₐ, SPKᵦ, T)`,
embeds T as DH3, queries the ROM on the resulting DH tuple to
get a session key, and passes it directly to the adversary.
+Why DH3? Among the four X3DH DH values, DH3 = ekₐ • SPKᵦ is the
Oh. While I was reading through this file, I was wondering why do we
embeds T as DH3 and not other DH. So wanted this paragraph to briefly
explains why DH3 was chosen to be embedded by T. Perhaps it is not clear in
my explanation. The following is an updated version of it:
"""
Why the reduction embeds T as DH3? The DDH challenge fixes two
group elements (A, B) whose discrete logs are hidden from the reduction;
these are installed as EKₐ and SPKᵦ in the simulated game, while ikₐ, ikᵦ,
opkᵦ are sampled by the reduction itself. Of the four DH values, three can
then be computed directly from
the public keys and the reduction's own scalars: DH1 = ikₐ • SPKᵦ uses
ikₐ, and DH2 = ekₐ • IKᵦ, DH4 = ekₐ • OPKᵦ are recovered via DH
commutativity as ikᵦ • EKₐ and opkᵦ • EKₐ. DH3 = ekₐ • SPKᵦ is the only one
requiring *both* hidden scalars — exactly the product ab • g that the
challenge T encodes. So T is embedded at DH3, and the rest of the tuple is
filled in honestly.
"""
WDYT? If you think providing more explanation may be even more confusing,
then we can simply remove this newly added paragraph completely.
—
Reply to this email directly, view it on GitHub
<#3 (comment)>,
or unsubscribe
<https://github.com/notifications/unsubscribe-auth/AFNNCEK6KLJIRS4ESFDP2WL4Y72LLAVCNFSM6AAAAACYDRT7XCVHI2DSMVQWIX3LMV43YUDVNRWFEZLROVSXG5CSMV3GSZLXHM2DEMJXGE2TAOJQHA>
.
You are receiving this because your review was requested.Message ID:
***@***.***>
|
2 participants
Summary
Documentation-only refinements made while reading through the X3DH-related files. Adds future-work notes to the primitive interfaces (KEM, AEAD), documents a notation convention in X3DH.lean, and expands explanations in the passive-secrecy game file.
No code/theorem changes — only comments, doc headers, and one cosmetic subscript fix.
Files changed
PQXDHLean/KEM.leanencaps/decaps, nokeygen(sufficient for correctness proofs)encapsand akeygenoperation, plus a suggested refactor pattern (separateKEMSpecalongsideKEM, mirroring theKDF/KDFOraclesplit)PQXDHLean/AEAD.leanencryptfor IND-CPASecurityDefs.leanPQXDHLean/X3DH/X3DH.leanF), uppercase names denote public keys (group elements inG), subscriptsₐ/ᵦindicate owner (Alice / Bob)SK_B→SKᵦ(matches existingSKₐ)PQXDHLean/X3DH/X3DHPassiveMessageSecrecy.leanSK(the KDF's output space)Tis embedded at DH3 specifically: DH3 =ekₐ • SPKᵦis the only DH value whose computation needs both secret scalars hidden in the DDH challenge; DH1/DH2/DH4 each involve at least one scalar the reduction samples itself